pcase

probabilistic process

P = pcase {

                     [prob1] : Q1

                     [prob2] : Q2

                     ...

                     default : Qn

                     };

It means process P has the probability prob1 to access Q1 process which can be a normal process or a probabilistic process too; in the same method we define prob2. At the end, default means P could get Qn with the remaining probability. To make sense, we define that all the transition probabilities' sum should be 1.

In addition, for user's convenience, we support another format of representing probabilities: Weighted pcase. It works as follows.

P = pcase {

                     weight1 : Q1

                     weight2 : Q2

                     ...

                     weightn : Qn

                     };

It means the probability from P to Q1 is weight1/(weight1+weight2+...+weightn). We take a simple case for example: the probabilites from P to Q1, Q2 and Q3 are 1/2, 1/3 and 1/6, so it can be represented by the following two methods.

P = pcase {

                     [0.5] : Q1

                     [0.333] : Q2

                     default : Q3

                     };

or

P = pcase {

                     3 : Q1

                     2 : Q2

                     1 : Q3

                     };

Using this kind of process and combined with normal nondeterministic processes in PAT, users could build probabilistic models as they want and check if the model satisfies some specific properties.